| Definitions | s(i;t).x, P   Q, False, A  B,  , {x:A| B(x)} ,  , x:A  B(x),  x:A. B(x),  , {T}, SQType(T), True, -n, P  Q, P & Q,  T, x:A  B(x), P Q, <a, b>, x,y:A//B(x;y), act(e), kind(e), Knd, (x  l), kind(a), Type, n+m, a < b, Void, KindDeq, deq-member(eq;x;L), IdDeq, Id, A c B, E, Atom$n, loc(e), time(e), w-info(w;e),  x.A(x), loc(e), kind(e), Action(i), IdLnk, f(x), x dom(f), mk-ma, x : v, f(x)?z, z != f(x) P(a;z), only members of L affect x :t, M.ds(x), M.bframe(k sends on l), M(i), @i: only L affects x : t, M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s), M.init(x,v), PossibleWorld(D;w), es_time(es), es_val(es), es-Trans(es), es_init(es), es-pred?(es), es_info(es), es-T(es), es_state_when(es;e), ES(the_w), (timed)state after e, kind(e), loc(e), E, vartype(i;x), FairFifo, World, D realizes2 es.P(es), e@i. P(e), @i only events in L change x : T, es is an event system of D, ES,  x. t(x), type List, D realizes es. P(es), #$n, r - s, r + s,  , s = t, s ~ t, vartype(i;x), a(i;t), isnull(a),  b,  A, (x when e), f(a), (x after e), state_after(e), t T, state_when(e) |